
#pragma once

#include "windows.h"
#include "windowsx.h"

#include <map>
#include <vector>
#include <list>
#include <stdexcept>
#include <algorithm>
#include <assert.h>

#include "constants.h"
#include "variable.h"
#include "literal.h"
#include "clause.h"
#include "problem_solver.h"
#include "istrategy.h"

namespace solver
{

	class problem_factory
	{
		std::vector<variable> variables;
		std::map<variable_name, variable_reference> variable_refs;
		std::vector<clause> clauses;

	public:

		problem_factory()
		{
			;
		}

		void clear()
		{
			variable_refs.clear();
			variables.clear();
			clauses.clear();
		}

	private:

		int declare(variable_name v)
		{
			int t = 0;
			if (variable_refs.count(v) == 0) {
				variable vx;
				vx.name = v;
				vx.ref = t = variables.size();
				vx.use_count = 1;
				variables.push_back(vx);
				variable_refs.insert(std::pair<variable_name, variable_reference>(v, t));
			}
			else
			{
				auto vid = variable_refs[v];
				auto& v = variables[vid];
				v.use_count++;
				t = vid;
			}
			return t;
		}

	public:

		void add_clause(int truth_func_id, int length, int *clause_rule, solver::istrategy* strategy)
		{
			// add a clause and add it to the deletes
			clause newClause;

			for (int i = 0; i < length; i++) {
				int v = clause_rule[i];
				int vn = strategy->int_to_name(v);
				variable_value vo = strategy->int_to_spin(v);
				variable_reference vr = declare(vn);
				literal nv;
				nv.ref = vr;
				nv.val = vo;
				newClause.literals.push_back(nv);
			}

			clauses.push_back(newClause);
		}

	public:

		int max_implication;
		std::list<pproduction> temp_production;

		void add_literal_production(problem_solver& new_problem, decision_string& match, literal& produced_lit)
		{
			production *new_production = new production();
			new_production->match = match;
			new_production->product = produced_lit;
			new_production->stringid = new_problem.production_index.add(match);
			temp_production.push_back(new_production);
			if (new_production->stringid > max_implication)
				max_implication = new_production->stringid;
		}

		void add_conflict_production(problem_solver& new_problem, decision_string& match)
		{
			literal conflict_lit;
			conflict_lit.ref = -1;
			conflict_lit.val = -1;
			conflict_lit.star = false;
			add_literal_production(new_problem, match, conflict_lit);
		}

		void create_problem(problem_solver& new_problem, int trace_variable, const char *problem_name)
		{

			int i = 0;
			int j = 0;
			int k = 0;

			new_problem.clear();
			new_problem.problem_name = problem_name;
			new_problem.problem_name += ".html";
			new_problem.variables.resize(variables.size());
			new_problem.production_index.clear();

			temp_production.clear();
			max_implication = 0;

			for (i = 0; i < variables.size(); i++)
			{
				auto& v = variables[i];
				auto& vd = new_problem.variables[v.ref];
				vd.ref = v.ref;
				vd.value = 0;
				vd.name = v.name;
				vd.values_used_mask = -1; // TODO: In the general case, this will need to come from the strategy
				
				// TODO: In the general case, this will need to be a permutation

				decision_string value_conflict_match;

				literal vx;
				vx.ref = v.ref;
				vx.star = false;
				vx.val = 0;
				value_conflict_match.add(vx);
				
				vx.val = 1;
				value_conflict_match.add(vx);

				add_conflict_production(new_problem, value_conflict_match);
			}

			new_problem.decisions.resize(clauses.size());

			for (i = 0; i < clauses.size(); i++)
			{
				auto &c = clauses[i];
				int num_literals = c.literals.size();
				decision_string conflict_match;

				// create the decision
				decision *d = new decision();
				new_problem.decisions[i] = d;

				j = 0;
				for (j = 0; j < num_literals; j++)
				{
					auto& lit = c.literals[j];
					d->literals.push_back(lit);
					new_problem.variables[lit.ref].values_used_mask &= ~(1 << lit.val);
				}

				// Build the implication graph
				// TODO: For generalized non-SAT problems,
				// this will need to be expanded for all
				// opposites, or a notation devised
				// to represent "all not" of a value.
				// Somewhere in the range of OverSAT check ins
				// this was done.

				for (j = 0; j < num_literals; j++)
				{
					literal implied = c.literals[j];					
					literal conflictlit = c.literals[j];

					decision_string implied_match;

					switch (conflictlit.val)
					{
					case 0:
						conflictlit.val = 1;
						break;
					case 1:
						conflictlit.val = 0;
						break;
					}

					conflict_match.add(conflictlit);

					int k = 0;
					for (k = 0; k < num_literals; k++)
					{
						if (k != j) 
						{
							literal newlit = c.literals[j];
							switch (newlit.val)
							{
							case 0:
								newlit.val = 1;
								break;
							case 1:
								newlit.val = 0;
								break;
							}
							implied_match.add(newlit);
						}
					}

					add_literal_production(new_problem, implied_match, implied);
				}

				add_conflict_production(new_problem, conflict_match);
			}

			// and finally, add conflicts for the unused variable assignments
			for (i = 0; i < new_problem.variables.size(); i++)
			{
				auto& vd = new_problem.variables[i];

				// TODO: again this will have to come from the strategy
				for (int j = 0; j < 2; j++)
				{
					decision_string unused_value_match;
					if (vd.values_used_mask & (1 << j)) 
					{
						literal l;
						l.ref = vd.ref;
						l.val = j;
						unused_value_match.add(l);
						add_conflict_production(new_problem, unused_value_match);
					}
				}
			}

			// wrap up the implication graph
			new_problem.productions.resize(max_implication + 1);
			for (i = 0; i < max_implication + 1; i++)
			{
				new_problem.productions[i] = nullptr;
			}

			for (auto& impi : temp_production)
			{
				new_problem.productions[impi->stringid] = impi;
			}

		}
	private:
	};
}
